Use the partial model for formula evaluation in Princess #528
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The partial model misses support for evaluating constant String formulas. The issue was reported and has already been fixed. We should remember to enable the test again in the next update uuverifiers/ostrich#108
…ultiple indices This is an issue with our backend and will be addressed separately See #520
This was referenced Oct 3, 2025
Member
|
Issues still not solved with Princess 2025-11-17 and Ostrich 2.0. We still need to wait for an updated version. UPDATE: The update of ostrich will be done with #565. Lets close this issue here. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hello,
We stopped using the partial model in Princess when we added support for Rationals and Strings. This was needed due to several issues with evaluation. Our current work-around is to simply push the formula that should be evaluated to the assertion stack, re-run the SAT check, and then report the values from the model. While this does work it adds additional overhead and makes our code harder to maintain
The evaluation issues in Princess have since been fixed, and this PR will therefore remove the current work-around and return to using the Princess partial model for evaluation
Currently there are still 2 failing tests that have been temporarily disabled in the last commits:
StringFormulaManagerTest.testOutputUnescapeThe partial model in Princess currently does not support evaluating constant String formulas. This issue was reported as Partial model does not evaluate String literals uuverifiers/ostrich#108 and has already been fixed upstream. We could wait for the next release, or just leave the test disabled for now. (--> see Princess: Handle String Literals in Evaluation of Partial Model #565)ModelTest.testGetArrays3This is a separate issue with our own backend that will be addressed in Add support for arrays with multiple indices in the Princess model #520. We can just leave the test disabled for now and turn it back on after the fix (--> see Add support for arrays with multiple indices in the Princess model #520)